/*
 * Copyright 2011 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.dnf;

import java.util.AbstractSet;

/**
 * 
 * A Clause is a set of Literals.
 * 
 * Because sets can be implemented in several ways this class is an abstract class. It extends
 * the Java AbstractSet class which is a skeleton implementation of the Set interface. It has a
 * additional method {@link #containsVariable(String)}.
 * 
 * It is not specified if the Clause class allows an occurrence of a variable with positive and negative
 * polarity (i.e. if a and &not;a are allowed to be in the clause). If it is not allowed this behavior
 * should be documented.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 */
public abstract class Clause extends AbstractSet<Literal>
{
	
	//public abstract boolean contains(Literal l);
	//public abstract Literal add(Literal l);
	//public abstract boolean remove(Literal l);
	//public abstract int size();
	
	/**
	 * Default constructor.
	 */
	public Clause()
	{
		;
	}
	
	/**
	 * This method returns true if the clause contains a Literal with identifier {@code name}
	 * either in positive or negative polarity.
	 * 
	 * @param name The identifier of the Literal.
	 * 
	 * @return The default implementation creates two new Literals (positive and negative polarity
	 * with identifier name) and checks if this Clause contains one of them. 
	 */
	public boolean containsVariable(String name)
	{
		return contains(new Literal(name)) || contains(new Literal(name, false));
	}
	
	/**
	 * Returns a String representation of this Clause in set notation (puts all Literals in curly brackets, separated by commas). 
	 * 
	 * @return "{l<sub>1</sub>, l<sub>2</sub>, &hellip;, l<sub>n</sub>}" where l<sub>1</sub>, l<sub>2</sub>, &hellip;, l<sub>n</sub>
	 * are the Literals in this Clause.
	 */
	public String toSetString()
	{
		StringBuilder result = new StringBuilder();
		result.append("{");
		boolean first = true;
		for(Literal l : this)
		{
			if(first)
			{
				first = false;
			}
			else
			{
				result.append(", ");
			}
			result.append(l);
		}
		result.append("}");
		return result.toString();
	}
	
	/**
	 * Returns a formula representation of this Clause.
	 * 
	 * @param separator The character that is used to separate the Literals.
	 * 
	 * @return "()" if this Clause is empty, "l" if this set is a singleton containing the Literal l
	 * and "(l<sub>1</sub> sep l<sub>2</sub> sep &hellip; sep l<sub>n</sub>)" if n &ge; 2 and l<sub>1</sub>, l<sub>2</sub>, &hellip;, l<sub>n</sub>
	 * are the elements in this Clause and sep is the given separator. 
	 */
	public String toFormulaString(char separator)
	{
		if(size() == 1)
		{
			for(Literal l : this)
				return l.toString();
		}
		StringBuilder result = new StringBuilder();
		result.append("(");
		boolean first = true;
		for(Literal l : this)
		{
			if(first)
			{
				first = false;
			}
			else
			{
				result.append(" ");
				result.append(separator);
				result.append(" ");
			}
			result.append(l);
		}
		result.append(")");
		return result.toString();
	}
	
	/**
	 * Returns the set String representation of this Clause as returned by {@link #toSetString()}.
	 * 
	 * @see #toSetString()
	 */
	@Override
	public String toString()
	{
		return toSetString();
	}
	
	/**
	 * Returns true if {@code other} is also a Clause and contains the same Literals as this Clause.
	 */
	@Override
	public boolean equals(Object other)
	{
		if(other == this)
			return true;
		if(!(other instanceof Clause))
			return false;
		Clause otherC = (Clause)other;
		if(this.size() != otherC.size())
			return false;
		for(Literal l : this)
		{
			if(!otherC.contains(l))
				return false;
		}
		return true;
	}
	
}
